0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 189 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 23 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇔, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇔, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
hC_in_g(c(0, 0)) → hC_out_g(c(0, 0))
hC_in_g(c(0, s(0))) → hC_out_g(c(0, s(0)))
hC_in_g(c(0, s(s(0)))) → hC_out_g(c(0, s(s(0))))
hC_in_g(c(0, s(s(s(0))))) → hC_out_g(c(0, s(s(s(0)))))
hC_in_g(c(0, s(s(s(s(0)))))) → hC_out_g(c(0, s(s(s(s(0))))))
hC_in_g(c(0, s(s(s(s(s(0))))))) → hC_out_g(c(0, s(s(s(s(s(0)))))))
hC_in_g(c(0, s(s(s(s(s(s(0)))))))) → hC_out_g(c(0, s(s(s(s(s(s(0))))))))
hC_in_g(c(0, s(s(s(s(s(s(s(0))))))))) → hC_out_g(c(0, s(s(s(s(s(s(s(0)))))))))
hC_in_g(c(0, s(s(s(s(s(s(s(s(T54)))))))))) → U3_g(T54, gA_in_gg(s(s(s(s(s(s(s(0))))))), T54))
gA_in_gg(T59, 0) → gA_out_gg(T59, 0)
gA_in_gg(T65, s(T70)) → U1_gg(T65, T70, gA_in_gg(s(T65), T70))
U1_gg(T65, T70, gA_out_gg(s(T65), T70)) → gA_out_gg(T65, s(T70))
U3_g(T54, gA_out_gg(s(s(s(s(s(s(s(0))))))), T54)) → hC_out_g(c(0, s(s(s(s(s(s(s(s(T54))))))))))
hC_in_g(c(s(T81), T77)) → U4_g(T81, T77, fB_in_gg(T81, T77))
fB_in_gg(0, T86) → fB_out_gg(0, T86)
fB_in_gg(s(T97), T93) → U2_gg(T97, T93, fB_in_gg(T97, s(T93)))
U2_gg(T97, T93, fB_out_gg(T97, s(T93))) → fB_out_gg(s(T97), T93)
U4_g(T81, T77, fB_out_gg(T81, T77)) → hC_out_g(c(s(T81), T77))
U4_g(T81, T77, fB_out_gg(T81, T77)) → U5_g(T81, T77, gA_in_gg(T81, T77))
U5_g(T81, T77, gA_out_gg(T81, T77)) → hC_out_g(c(s(T81), T77))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
hC_in_g(c(0, 0)) → hC_out_g(c(0, 0))
hC_in_g(c(0, s(0))) → hC_out_g(c(0, s(0)))
hC_in_g(c(0, s(s(0)))) → hC_out_g(c(0, s(s(0))))
hC_in_g(c(0, s(s(s(0))))) → hC_out_g(c(0, s(s(s(0)))))
hC_in_g(c(0, s(s(s(s(0)))))) → hC_out_g(c(0, s(s(s(s(0))))))
hC_in_g(c(0, s(s(s(s(s(0))))))) → hC_out_g(c(0, s(s(s(s(s(0)))))))
hC_in_g(c(0, s(s(s(s(s(s(0)))))))) → hC_out_g(c(0, s(s(s(s(s(s(0))))))))
hC_in_g(c(0, s(s(s(s(s(s(s(0))))))))) → hC_out_g(c(0, s(s(s(s(s(s(s(0)))))))))
hC_in_g(c(0, s(s(s(s(s(s(s(s(T54)))))))))) → U3_g(T54, gA_in_gg(s(s(s(s(s(s(s(0))))))), T54))
gA_in_gg(T59, 0) → gA_out_gg(T59, 0)
gA_in_gg(T65, s(T70)) → U1_gg(T65, T70, gA_in_gg(s(T65), T70))
U1_gg(T65, T70, gA_out_gg(s(T65), T70)) → gA_out_gg(T65, s(T70))
U3_g(T54, gA_out_gg(s(s(s(s(s(s(s(0))))))), T54)) → hC_out_g(c(0, s(s(s(s(s(s(s(s(T54))))))))))
hC_in_g(c(s(T81), T77)) → U4_g(T81, T77, fB_in_gg(T81, T77))
fB_in_gg(0, T86) → fB_out_gg(0, T86)
fB_in_gg(s(T97), T93) → U2_gg(T97, T93, fB_in_gg(T97, s(T93)))
U2_gg(T97, T93, fB_out_gg(T97, s(T93))) → fB_out_gg(s(T97), T93)
U4_g(T81, T77, fB_out_gg(T81, T77)) → hC_out_g(c(s(T81), T77))
U4_g(T81, T77, fB_out_gg(T81, T77)) → U5_g(T81, T77, gA_in_gg(T81, T77))
U5_g(T81, T77, gA_out_gg(T81, T77)) → hC_out_g(c(s(T81), T77))
HC_IN_G(c(0, s(s(s(s(s(s(s(s(T54)))))))))) → U3_G(T54, gA_in_gg(s(s(s(s(s(s(s(0))))))), T54))
HC_IN_G(c(0, s(s(s(s(s(s(s(s(T54)))))))))) → GA_IN_GG(s(s(s(s(s(s(s(0))))))), T54)
GA_IN_GG(T65, s(T70)) → U1_GG(T65, T70, gA_in_gg(s(T65), T70))
GA_IN_GG(T65, s(T70)) → GA_IN_GG(s(T65), T70)
HC_IN_G(c(s(T81), T77)) → U4_G(T81, T77, fB_in_gg(T81, T77))
HC_IN_G(c(s(T81), T77)) → FB_IN_GG(T81, T77)
FB_IN_GG(s(T97), T93) → U2_GG(T97, T93, fB_in_gg(T97, s(T93)))
FB_IN_GG(s(T97), T93) → FB_IN_GG(T97, s(T93))
U4_G(T81, T77, fB_out_gg(T81, T77)) → U5_G(T81, T77, gA_in_gg(T81, T77))
U4_G(T81, T77, fB_out_gg(T81, T77)) → GA_IN_GG(T81, T77)
hC_in_g(c(0, 0)) → hC_out_g(c(0, 0))
hC_in_g(c(0, s(0))) → hC_out_g(c(0, s(0)))
hC_in_g(c(0, s(s(0)))) → hC_out_g(c(0, s(s(0))))
hC_in_g(c(0, s(s(s(0))))) → hC_out_g(c(0, s(s(s(0)))))
hC_in_g(c(0, s(s(s(s(0)))))) → hC_out_g(c(0, s(s(s(s(0))))))
hC_in_g(c(0, s(s(s(s(s(0))))))) → hC_out_g(c(0, s(s(s(s(s(0)))))))
hC_in_g(c(0, s(s(s(s(s(s(0)))))))) → hC_out_g(c(0, s(s(s(s(s(s(0))))))))
hC_in_g(c(0, s(s(s(s(s(s(s(0))))))))) → hC_out_g(c(0, s(s(s(s(s(s(s(0)))))))))
hC_in_g(c(0, s(s(s(s(s(s(s(s(T54)))))))))) → U3_g(T54, gA_in_gg(s(s(s(s(s(s(s(0))))))), T54))
gA_in_gg(T59, 0) → gA_out_gg(T59, 0)
gA_in_gg(T65, s(T70)) → U1_gg(T65, T70, gA_in_gg(s(T65), T70))
U1_gg(T65, T70, gA_out_gg(s(T65), T70)) → gA_out_gg(T65, s(T70))
U3_g(T54, gA_out_gg(s(s(s(s(s(s(s(0))))))), T54)) → hC_out_g(c(0, s(s(s(s(s(s(s(s(T54))))))))))
hC_in_g(c(s(T81), T77)) → U4_g(T81, T77, fB_in_gg(T81, T77))
fB_in_gg(0, T86) → fB_out_gg(0, T86)
fB_in_gg(s(T97), T93) → U2_gg(T97, T93, fB_in_gg(T97, s(T93)))
U2_gg(T97, T93, fB_out_gg(T97, s(T93))) → fB_out_gg(s(T97), T93)
U4_g(T81, T77, fB_out_gg(T81, T77)) → hC_out_g(c(s(T81), T77))
U4_g(T81, T77, fB_out_gg(T81, T77)) → U5_g(T81, T77, gA_in_gg(T81, T77))
U5_g(T81, T77, gA_out_gg(T81, T77)) → hC_out_g(c(s(T81), T77))
HC_IN_G(c(0, s(s(s(s(s(s(s(s(T54)))))))))) → U3_G(T54, gA_in_gg(s(s(s(s(s(s(s(0))))))), T54))
HC_IN_G(c(0, s(s(s(s(s(s(s(s(T54)))))))))) → GA_IN_GG(s(s(s(s(s(s(s(0))))))), T54)
GA_IN_GG(T65, s(T70)) → U1_GG(T65, T70, gA_in_gg(s(T65), T70))
GA_IN_GG(T65, s(T70)) → GA_IN_GG(s(T65), T70)
HC_IN_G(c(s(T81), T77)) → U4_G(T81, T77, fB_in_gg(T81, T77))
HC_IN_G(c(s(T81), T77)) → FB_IN_GG(T81, T77)
FB_IN_GG(s(T97), T93) → U2_GG(T97, T93, fB_in_gg(T97, s(T93)))
FB_IN_GG(s(T97), T93) → FB_IN_GG(T97, s(T93))
U4_G(T81, T77, fB_out_gg(T81, T77)) → U5_G(T81, T77, gA_in_gg(T81, T77))
U4_G(T81, T77, fB_out_gg(T81, T77)) → GA_IN_GG(T81, T77)
hC_in_g(c(0, 0)) → hC_out_g(c(0, 0))
hC_in_g(c(0, s(0))) → hC_out_g(c(0, s(0)))
hC_in_g(c(0, s(s(0)))) → hC_out_g(c(0, s(s(0))))
hC_in_g(c(0, s(s(s(0))))) → hC_out_g(c(0, s(s(s(0)))))
hC_in_g(c(0, s(s(s(s(0)))))) → hC_out_g(c(0, s(s(s(s(0))))))
hC_in_g(c(0, s(s(s(s(s(0))))))) → hC_out_g(c(0, s(s(s(s(s(0)))))))
hC_in_g(c(0, s(s(s(s(s(s(0)))))))) → hC_out_g(c(0, s(s(s(s(s(s(0))))))))
hC_in_g(c(0, s(s(s(s(s(s(s(0))))))))) → hC_out_g(c(0, s(s(s(s(s(s(s(0)))))))))
hC_in_g(c(0, s(s(s(s(s(s(s(s(T54)))))))))) → U3_g(T54, gA_in_gg(s(s(s(s(s(s(s(0))))))), T54))
gA_in_gg(T59, 0) → gA_out_gg(T59, 0)
gA_in_gg(T65, s(T70)) → U1_gg(T65, T70, gA_in_gg(s(T65), T70))
U1_gg(T65, T70, gA_out_gg(s(T65), T70)) → gA_out_gg(T65, s(T70))
U3_g(T54, gA_out_gg(s(s(s(s(s(s(s(0))))))), T54)) → hC_out_g(c(0, s(s(s(s(s(s(s(s(T54))))))))))
hC_in_g(c(s(T81), T77)) → U4_g(T81, T77, fB_in_gg(T81, T77))
fB_in_gg(0, T86) → fB_out_gg(0, T86)
fB_in_gg(s(T97), T93) → U2_gg(T97, T93, fB_in_gg(T97, s(T93)))
U2_gg(T97, T93, fB_out_gg(T97, s(T93))) → fB_out_gg(s(T97), T93)
U4_g(T81, T77, fB_out_gg(T81, T77)) → hC_out_g(c(s(T81), T77))
U4_g(T81, T77, fB_out_gg(T81, T77)) → U5_g(T81, T77, gA_in_gg(T81, T77))
U5_g(T81, T77, gA_out_gg(T81, T77)) → hC_out_g(c(s(T81), T77))
FB_IN_GG(s(T97), T93) → FB_IN_GG(T97, s(T93))
hC_in_g(c(0, 0)) → hC_out_g(c(0, 0))
hC_in_g(c(0, s(0))) → hC_out_g(c(0, s(0)))
hC_in_g(c(0, s(s(0)))) → hC_out_g(c(0, s(s(0))))
hC_in_g(c(0, s(s(s(0))))) → hC_out_g(c(0, s(s(s(0)))))
hC_in_g(c(0, s(s(s(s(0)))))) → hC_out_g(c(0, s(s(s(s(0))))))
hC_in_g(c(0, s(s(s(s(s(0))))))) → hC_out_g(c(0, s(s(s(s(s(0)))))))
hC_in_g(c(0, s(s(s(s(s(s(0)))))))) → hC_out_g(c(0, s(s(s(s(s(s(0))))))))
hC_in_g(c(0, s(s(s(s(s(s(s(0))))))))) → hC_out_g(c(0, s(s(s(s(s(s(s(0)))))))))
hC_in_g(c(0, s(s(s(s(s(s(s(s(T54)))))))))) → U3_g(T54, gA_in_gg(s(s(s(s(s(s(s(0))))))), T54))
gA_in_gg(T59, 0) → gA_out_gg(T59, 0)
gA_in_gg(T65, s(T70)) → U1_gg(T65, T70, gA_in_gg(s(T65), T70))
U1_gg(T65, T70, gA_out_gg(s(T65), T70)) → gA_out_gg(T65, s(T70))
U3_g(T54, gA_out_gg(s(s(s(s(s(s(s(0))))))), T54)) → hC_out_g(c(0, s(s(s(s(s(s(s(s(T54))))))))))
hC_in_g(c(s(T81), T77)) → U4_g(T81, T77, fB_in_gg(T81, T77))
fB_in_gg(0, T86) → fB_out_gg(0, T86)
fB_in_gg(s(T97), T93) → U2_gg(T97, T93, fB_in_gg(T97, s(T93)))
U2_gg(T97, T93, fB_out_gg(T97, s(T93))) → fB_out_gg(s(T97), T93)
U4_g(T81, T77, fB_out_gg(T81, T77)) → hC_out_g(c(s(T81), T77))
U4_g(T81, T77, fB_out_gg(T81, T77)) → U5_g(T81, T77, gA_in_gg(T81, T77))
U5_g(T81, T77, gA_out_gg(T81, T77)) → hC_out_g(c(s(T81), T77))
FB_IN_GG(s(T97), T93) → FB_IN_GG(T97, s(T93))
FB_IN_GG(s(T97), T93) → FB_IN_GG(T97, s(T93))
From the DPs we obtained the following set of size-change graphs:
GA_IN_GG(T65, s(T70)) → GA_IN_GG(s(T65), T70)
hC_in_g(c(0, 0)) → hC_out_g(c(0, 0))
hC_in_g(c(0, s(0))) → hC_out_g(c(0, s(0)))
hC_in_g(c(0, s(s(0)))) → hC_out_g(c(0, s(s(0))))
hC_in_g(c(0, s(s(s(0))))) → hC_out_g(c(0, s(s(s(0)))))
hC_in_g(c(0, s(s(s(s(0)))))) → hC_out_g(c(0, s(s(s(s(0))))))
hC_in_g(c(0, s(s(s(s(s(0))))))) → hC_out_g(c(0, s(s(s(s(s(0)))))))
hC_in_g(c(0, s(s(s(s(s(s(0)))))))) → hC_out_g(c(0, s(s(s(s(s(s(0))))))))
hC_in_g(c(0, s(s(s(s(s(s(s(0))))))))) → hC_out_g(c(0, s(s(s(s(s(s(s(0)))))))))
hC_in_g(c(0, s(s(s(s(s(s(s(s(T54)))))))))) → U3_g(T54, gA_in_gg(s(s(s(s(s(s(s(0))))))), T54))
gA_in_gg(T59, 0) → gA_out_gg(T59, 0)
gA_in_gg(T65, s(T70)) → U1_gg(T65, T70, gA_in_gg(s(T65), T70))
U1_gg(T65, T70, gA_out_gg(s(T65), T70)) → gA_out_gg(T65, s(T70))
U3_g(T54, gA_out_gg(s(s(s(s(s(s(s(0))))))), T54)) → hC_out_g(c(0, s(s(s(s(s(s(s(s(T54))))))))))
hC_in_g(c(s(T81), T77)) → U4_g(T81, T77, fB_in_gg(T81, T77))
fB_in_gg(0, T86) → fB_out_gg(0, T86)
fB_in_gg(s(T97), T93) → U2_gg(T97, T93, fB_in_gg(T97, s(T93)))
U2_gg(T97, T93, fB_out_gg(T97, s(T93))) → fB_out_gg(s(T97), T93)
U4_g(T81, T77, fB_out_gg(T81, T77)) → hC_out_g(c(s(T81), T77))
U4_g(T81, T77, fB_out_gg(T81, T77)) → U5_g(T81, T77, gA_in_gg(T81, T77))
U5_g(T81, T77, gA_out_gg(T81, T77)) → hC_out_g(c(s(T81), T77))
GA_IN_GG(T65, s(T70)) → GA_IN_GG(s(T65), T70)
GA_IN_GG(T65, s(T70)) → GA_IN_GG(s(T65), T70)
From the DPs we obtained the following set of size-change graphs: